00100 PRE_PRED: P,G; 00200 VAR:x,y,z; 00300 G1: ∀(x,y)(P(x,y) ∧P(y,z) ⊃ G(x,z)); 00400 G2: ∀y∃x P(x,y); 00500 THEOREM: ∃(x,y)G(x,y); ;